\begin{tabbing}
input{-}forwarding\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Sys}$; ${\it isupdate}$; ${\it In}$; $f$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex](($\uparrow$($e$ $\in_{b}$ ${\it In}$)) $\Rightarrow$ (${\it Sys}$($e$) = [${\it In}$($e$) / []] $\in$ (${\it Cmd}$ List)))
\\[0ex]\& (\=($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$)))\+
\\[0ex]$\Rightarrow$ ($\neg$(es{-}loc(${\it es}$; ($f$($e$))) = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\Rightarrow$ \=((\=($\exists$\=${\it e'}$:es{-}E{-}interface(${\it es}$;${\it Sys}$)\+\+\+
\\[0ex](es{-}locl(${\it es}$; ${\it e'}$; $e$) \& es{-}loc(${\it es}$; ($f$(${\it e'}$))) = es{-}loc(${\it es}$; ($f$($e$))) $\in$ Id))
\-\\[0ex]$\Rightarrow$ (${\it Sys}$($e$) = ${\it Sys}$($f$($e$)) $\in$ (${\it Cmd}$ List)))
\-\\[0ex]\& (\=($\neg$($\exists$\=${\it e'}$:es{-}E{-}interface(${\it es}$;${\it Sys}$)\+\+
\\[0ex](es{-}locl(${\it es}$; ${\it e'}$; $e$) \& es{-}loc(${\it es}$; ($f$(${\it e'}$))) = es{-}loc(${\it es}$; ($f$($e$))) $\in$ Id)))
\-\\[0ex]$\Rightarrow$ (\=${\it Sys}$($e$)\+
\\[0ex]=
\\[0ex]if $e$ $\in_{b}$ es{-}prior{-}interface\{i:l\}(${\it es}$; ${\it Sys}$)
\\[0ex]then nth\_tl(\=$\parallel$filter\=(${\it isupdate}$\+\+
\\[0ex];es{-}interface{-}history(\=${\it es}$;\+
\\[0ex]${\it Sys}$;
\\[0ex]es{-}prior{-}interface\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Sys}$)($e$)
\-\\[0ex]))$\parallel$;
\-\-\\[0ex]filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; ($f$($e$)))))
\-\\[0ex]else filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; ($f$($e$))))
\\[0ex]fi 
\\[0ex]$\in$ (${\it Cmd}$ List)))))
\-\-\-\-\\[0ex]\& (\=($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$)))\+
\\[0ex]$\Rightarrow$ (es{-}loc(${\it es}$; ($f$($e$))) = es{-}loc(${\it es}$; $e$) $\in$ Id)
\\[0ex]$\Rightarrow$ (${\it Sys}$($e$) = [] $\in$ (${\it Cmd}$ List)))
\-\\[0ex]\& (\=did{-}forward(${\it es}$; ${\it Sys}$; $f$; $e$)\+
\\[0ex]$\Rightarrow$ \=($\forall$$a$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex]es{-}locl(${\it es}$; $a$; $e$)
\\[0ex]$\Rightarrow$ should{-}forward(${\it es}$; ${\it In}$; ${\it isupdate}$; $f$; $a$)
\\[0ex]$\Rightarrow$ did{-}forward(${\it es}$; ${\it Sys}$; $f$; $a$)))
\-\-\-
\end{tabbing}